package controlGraph;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.Queue;

public class ArithExpr extends Expression{
	private String rop;
	private Expression lhs;
	private Expression rhs;
	
	public ArithExpr(String crop, Expression clhs, Expression crhs){
		rop = crop;
		lhs = clhs;
		rhs = crhs;
		
		//THIS CODE SHOULD BE PLACED IN A DIFFERENT PLACE.
		/*if(lhs instanceof ArrayRef){
			ArrayRef temp = (ArrayRef) lhs;
			String variable_name = temp.getVariable();
			Expression index = temp.getIndexExpression();
			ArrayList<String> empty = new ArrayList<String>();
			Expression Oldvalue = null;
			if(Statement.getResult(variable_name, index, empty)){
				System.out.println("The array access in "+variable_name+" is valid");
			}
			else{
				System.out.println("This array reference is unsatisfiable");
				System.exit(1);
			}
		}
		
		if(rhs instanceof ArrayRef){
			ArrayRef temp = (ArrayRef) rhs;
			String variable_name = temp.getVariable();
			Expression index = temp.getIndexExpression();
			ArrayList<String> empty = new ArrayList<String>();
			Expression Oldvalue = null;
			if(Statement.getResult(variable_name, index, empty)){
				System.out.println("The array access in "+variable_name+" is valid");
			}
			else{
				System.out.println("This array reference is unsatisfiable");
				System.exit(1);
			}
		}*/
	}
	
	public String getOper(){
		return this.rop;
	}
	
	public Expression getLHS(){
		return this.lhs;
	}
	
	public Expression getRHS(){
		return this.rhs;
	}
	
	public boolean equals(Object one){
		
		boolean b1 = false;
		boolean b2 = false;
		boolean b3 = false;
		
		if(one instanceof ArithExpr){
			b1 = (((ArithExpr)one).getOper().compareTo(this.rop) == 0);
			b2 = (((ArithExpr)one).getLHS().isSame(this.lhs));
			b3 = (((ArithExpr)one).getRHS().isSame(this.rhs));
		}
		return (b1 & b2 && b3);
	}
	
	public int hashCode(){
		int hash = 701;
		
		String temp = rop;
		
		for(int i=0;i<temp.length();i++){
			hash = hash * temp.charAt(i) * 11;
		}
		
		temp = lhs.toString();
		for(int i=0;i<temp.length();i++){
			hash = hash * temp.charAt(i) * 31;
		}
		
		temp = rhs.toString();
		for(int i=0;i<temp.length();i++){
			hash = hash * temp.charAt(i) * 7;
		}
		
		return hash;
	}
	
	//When passed the expression , will say if the expression is part of the ArithExpr
	public boolean containsExpression(Expression e){
		return ((this.getLHS()).equals(e) || (this.getRHS()).equals(e));
	}

	@Override
	public String toString() {
		return lhs.toString()+ " "+rop+ " "+ rhs.toString();
	}
	
	public ArithExpr getOppoAxiom(){
		if(rop.compareToIgnoreCase("==") == 0 || rop.compareToIgnoreCase("!=")==0){
			System.out.println("The relational operators == and != are not included in the grammar");
			System.exit(1);
		}
		
		//if the rop is not any of the below then it is a error
		if(rop.compareToIgnoreCase("<=")!=0 && rop.compareToIgnoreCase("<")!=0 &&
				rop.compareToIgnoreCase(">=")!=0 && rop.compareToIgnoreCase(">")!=0)
		{
			System.out.println("This "+rop+" is not allowed as a relational operator");
		}
		
		String rel="";
		if(rop.compareToIgnoreCase("<=") == 0)
			rel = ">";
		if(rop.compareToIgnoreCase(">=") == 0)
			rel = "<";
		if(rop.compareToIgnoreCase("<") == 0)
			rel = ">=";
		if(rop.compareToIgnoreCase(">") == 0)
			rel = "<=";
		
		ArithExpr ret = new ArithExpr(rel,lhs,rhs);
		
		return ret;
	}
	
	//Grammar cannot contain the != && == sign as a relational operator due to Z3's missing capability
	public String getAxiomString(){
		if(rop.compareToIgnoreCase("==") == 0 || rop.compareToIgnoreCase("!=")==0){
			System.out.println("The relational operators == and != are not included in the grammar");
			System.exit(1);
		}
		
		//if the rop is not any of the below then it is a error
		if(rop.compareToIgnoreCase("<=")!=0 && rop.compareToIgnoreCase("<")!=0 &&
				rop.compareToIgnoreCase(">=")!=0 && rop.compareToIgnoreCase(">")!=0)
		{
			System.out.println("This "+rop+" is not allowed as a relational operator");
		}
		return rop+" "+lhs+" "+rhs;
	}
	
	/*public String getOppoAxiomString(){
		if(rop.compareToIgnoreCase("==") == 0 || rop.compareToIgnoreCase("!=")==0){
			System.out.println("The relational operators == and != are not included in the grammar");
			System.exit(1);
		}
		
		//if the rop is not any of the below then it is a error
		if(rop.compareToIgnoreCase("<=")!=0 && rop.compareToIgnoreCase("<")!=0 &&
				rop.compareToIgnoreCase(">=")!=0 && rop.compareToIgnoreCase(">")!=0)
		{
			System.out.println("This "+rop+" is not allowed as a relational operator");
		}
		
		String rel="";
		if(rop.compareToIgnoreCase("<=") == 0)
			rel = ">";
		if(rop.compareToIgnoreCase(">=") == 0)
			rel = "<";
		if(rop.compareToIgnoreCase("<") == 0)
			rel = ">=";
		if(rop.compareToIgnoreCase(">") == 0)
			rel = "<=";
		
		return rel+" "+lhs+" "+rhs;
	}*/

	public void addAxiomsForExpression(ArrayList<String> axioms, Expression currExpr, String name,
			HashSet<Expression> finished, HashSet<ArithExpr> RuleSet) {
		// TODO Auto-generated method stub
		
		//If the rule contains the expression then we have to generate the axiom and add it 
		//if(containsExpression(currExpr)){
		if((lhs.equals(currExpr) && (rhs.equals(currExpr))) ||
			(lhs.equals(currExpr) && (!finished.contains(rhs))) ||
			((!finished.contains(lhs)) && rhs.equals(rhs))){
			String addIt = "(assert ("+ this.rop+" ";
			
			//If the expression is the lhs ,print the name
			if(lhs.equals(currExpr)){
				addIt = addIt+name+" ";
			}
			else{
				if(lhs instanceof LValueInt){
					addIt = addIt+((LValueInt)lhs).getValue()+" ";
				}
				
				if(lhs instanceof Variable){
					Variable temp = ((Variable)lhs);
					String VariName = temp.getVariable();
					StoreValue value = Statement.zigma.getStoreValue(VariName);
					
					//If the variable is never declared !!!
					if(value == null){
						System.out.println("Compiler error: No Variable "+VariName+" defined");
						System.exit(1);
					}
					
					Expression e = value.getExpression();
					if(e instanceof UndefinedExpression){
						Statement.addAxiomsForExpression(axioms, currExpr.toString(), lhs, finished, RuleSet);
						addIt = addIt+currExpr.toString()+" ";
					}
					
					if(e instanceof LValueInt){
						addIt = addIt+((LValueInt) (e)).getValue()+" ";
					}
					
					if(!((e instanceof LValueInt) || (e instanceof UndefinedExpression))){
						System.out.println("Error : The stored Expression for the variable "+VariName+"  doesn't have a LValueInt stored");
						System.exit(1);
					}
				}
				
				//If ArrayRef is a part of the Rules, then it means that array reference is valid
				// But the value of the ArrayRef might be valid or Undefined
				if(lhs instanceof ArrayRef){
					Expression indexValue = Statement.zigma.getLValueInt(lhs);
					
					if(indexValue instanceof LValueInt){
						addIt = addIt+((LValueInt) (indexValue)).getValue()+" ";
					}
					
					if(indexValue instanceof UndefinedExpression){
						Statement.addAxiomsForExpression(axioms, currExpr.toString(), lhs, finished, RuleSet);
						addIt = addIt+currExpr.toString()+" ";
					}
					if(!((indexValue instanceof LValueInt) || (indexValue instanceof UndefinedExpression))){
						System.out.println("Error : The stored Expression for the variable "+((ArrayRef)lhs).getVariable()+"  doesn't have a LValueInt stored");
						System.exit(1);
					}
				}
			}//end - else if(lhs.equals(currExpr)
			
			//If the expression is the rhs ,print the name
			if(rhs.equals(currExpr)){
				addIt = addIt+name+"))";
			}
			else{
				if(rhs instanceof LValueInt){
					addIt = addIt+((LValueInt)rhs).getValue()+"))";
				}
				
				if(rhs instanceof Variable){
					Variable temp = ((Variable)rhs);
					String VariName = temp.getVariable();
					StoreValue value = Statement.zigma.getStoreValue(VariName);
					
					//If the variable is never declared !!!
					if(value == null){
						System.out.println("Compiler error: No Variable "+VariName+" defined");
						System.exit(1);
					}
					
					Expression e = value.getExpression();
					if(e instanceof UndefinedExpression){
						Statement.addAxiomsForExpression(axioms, currExpr.toString(), rhs, finished, RuleSet);
						addIt = addIt+currExpr.toString()+"))";
					}
					
					if(e instanceof LValueInt){
						addIt = addIt+((LValueInt) (e)).getValue()+"))";
					}
					
					if(!((e instanceof LValueInt) || (e instanceof UndefinedExpression))){
						System.out.println("Error : The stored Expression for the variable "+VariName+"  doesn't have a LValueInt stored");
						System.exit(1);
					}
				}
				
				//If ArrayRef is a part of the Rules, then it means that array reference is valid
				// But the value of the ArrayRef might be valid or Undefined
				if(rhs instanceof ArrayRef){
					Expression indexValue = Statement.zigma.getLValueInt(rhs);
					
					if(indexValue instanceof LValueInt){
						addIt = addIt+((LValueInt) (indexValue)).getValue()+"))";
					}
					
					if(indexValue instanceof UndefinedExpression){
						Statement.addAxiomsForExpression(axioms, currExpr.toString(), rhs, finished, RuleSet);
						addIt = addIt+currExpr.toString()+"))";
					}
					if(!((indexValue instanceof LValueInt) || (indexValue instanceof UndefinedExpression))){
						System.out.println("Error : The stored Expression for the variable "+((ArrayRef)rhs).getVariable()+"  doesn't have a LValueInt stored");
						System.exit(1);
					}
				}
			}//end - else if(rhs.equals(currExpr)
			
			axioms.add(addIt);
		}		
	}

	public boolean canRemove(Expression e) {
		// TODO Auto-generated method stub
		
		if(e instanceof ArrayRef){
			return (lhs.equals(e) || rhs.equals(e));
		}
		
		boolean b1 = false;
		if(lhs instanceof Variable){
			b1 = lhs.equals(e);
		}
		if(lhs instanceof ArrayRef){
			b1=((ArrayRef)lhs).getVariableExpression().equals(e);
		}
		
		boolean b2 = false;
		if(rhs instanceof Variable){
			b2 = rhs.equals(e);
		}
		if(rhs instanceof ArrayRef){
			b2=((ArrayRef)rhs).getVariableExpression().equals(e);
		}
		
		return (b1 || b2);
	}

	public boolean isValid() {
		// TODO Auto-generated method stub
		
		//The below two variables are not used. But the getLValueInt() will
		//the validity of the expression i.e. It will just see if the expressions 
		//independently are valid
		Expression forLHS = Statement.zigma.getLValueInt(lhs);
		Expression forRHS = Statement.zigma.getLValueInt(rhs);
		return true;
	}
}
